Nuprl Lemma : set_leq_weakening_eq 13,42

s:QOSet, ab:|s|. (a = b (a  b
latex


Upsets 1
Definitions of StatementDSet, QOSet
Definitions, t  T, P  Q, x:AB(x), DSet, QOSet
Lemmasqoset wf, set car wf, set leq wf, qoset refl

origin